es:ES, e':E, P:({e:E| loc(e) = loc(e')  Id} ). e@loc(e'). Dec(P(e))  Dec(ee'.P(e)) 

latex

Definitions	x(s), e<e'.P(e), Dec(P), P  Q, P  Q, x. t(x), x:A. B(x), t  T, loc(e), Id, E, , ee'.P(e), P  Q, P & Q, P  Q, ES, e@i. P(e)
Lemmas	alle-at wf, decidable wf, event system wf, decidable functionality, existse-le-iff, existse-le wf, existse-before wf, es-E wf, Id wf, es-loc wf, decidable or, decidable existse-before